1. $T$ : Type
\\[0ex]2. $T$ List
\\[0ex]3. $x$ : $T$
\\[0ex]4. $y$ : $T$
\\[0ex]5. no\_repeats($T$;[])
\\[0ex]6. adjacent($T$;[];$x$;$y$)
\\[0ex]7. $z$ : $T$
\\[0ex]8. $z$ before $y$ $\in$ []
\\[0ex]$\vdash$  $z$ before $x$ $\in$ [] $\vee$ ($z$ = $x$)